# -*- coding: utf-8 -*-
# created on 2016/11/30
from mathsolver.functions.shulie.QianNXiangHe import ShuLieQiuHe
from mathsolver.functions.base import *
from mathsolver.functions.shulie.Fundamental import *
from sympy.abc import n
from mathsolver.functions.shulie.ShuLie_getSeqPoly import ShuLieGetSeqPoly
from sympy import together, fraction


def inf_sums_items(expr):
    items = []
    expr_left = expr[:expr.find("\u2026") - 1]
    expr_left = sympify(expr_left)
    expr_right = expr[expr.find("\u2026") + 2:]
    expr_right = sympify(expr_right)
    for expr_left_item in expr_left.args:
        items.append(expr_left_item)
    items.append(None)
    if expr_right.is_Add:
        for expr_right_item in expr_right:
            items.append(expr_right_item)
    else:
        items.append(expr_right)
    return items


def judge_exp_fangsuo001(expr):
    answer = False
    expr = together(expr)
    fenzhi, fenmu = fraction(expr)
    fenzhi_symbols = fenzhi.free_symbols
    fenmu_p = None
    fenmu_q = None
    fenmu_exp = None
    if (n not in fenzhi_symbols) and fenmu.is_Add and (len(fenmu.args) == 2):
        first_part, second_part = fenmu.args
        if (n not in first_part.free_symbols) and (n in second_part.free_symbols):
            if (first_part < 0) and (isinstance(second_part, Pow)):
                _base, exp = second_part.args
                if _base > - first_part:
                    answer = True
                    fenmu_p = _base
                    fenmu_q = - first_part
                    fenmu_exp = exp
    return answer, fenmu_p, fenmu_q, fenmu_exp


def judge_fraction_fangsuo001(expr):
    answer = False
    expr = together(expr)
    fenzhi, fenmu = fraction(expr)
    fenmu = fenmu.factor()
    fenzhi_symbols = fenzhi.free_symbols
    if n not in fenzhi_symbols:
        if isinstance(fenmu, Pow) and fenmu.args[1] == 2:
            fenmu_base = fenmu.args[0]
            if str(fenmu_base) == str('n'):
                answer = True
    return answer, fenzhi, fenmu


def solve_shulie_ineq(ineq):
    min_answer = None
    left, op, right = ineq
    for i in range(1, 100):
        new_left = left.subs({n: i})
        new_right = right.subs({n: i})
        if Rel(new_left, new_right, op):
            min_answer = i
            break
    return min_answer


class ShuLieProveIneq001(BaseFunction):
    """
    已知数列{a_{n}}满足a_{1}=1,a_{n+1}=3a_{n}+1.证明:\\frac{1}{{a}_{1}}+\\frac{1}{{a}_{2}}+…+\\frac{1}{{a}_{n}}<\\frac{3}{2}.
    """
    def solver(self, *args):
        assert len(args) == 1
        assert isinstance(args[0], BaseSeqIneq)
        left, op, right = args[0].value
        right = sympify(right)
        assert "\u2026" in left
        left_items = inf_sums_items(left)
        left_an = left_items[-1]
        stepsolver1 = ShuLieGetSeqPoly(self.known).solver(BasePoly(left_an))
        self.steps += stepsolver1.steps
        self.label.update(stepsolver1.label)
        left_an_values = stepsolver1.output[0].sympify()
        assert len(left_an_values) == 1
        left_an_value = left_an_values[0]
        left_a1_value = left_an_value.subs({n: 1})
        if Rel(left_a1_value, right, op):
            self.steps.append(["", "当%s = 1时,不等式成立" % (new_latex(n))])
        left_an_value_flag, left_an_value_p, left_an_value_q, left_an_value_exp = judge_exp_fangsuo001(left_an_value)
        assert left_an_value_flag
        left_an_value_fenzhi, left_an_value_fenmu = fraction(left_an_value)
        new_left_an_value_fenmu = left_an_value_p ** left_an_value_exp - left_an_value_p ** (left_an_value_exp - 1)
        new_left_an_value = left_an_value_fenzhi / new_left_an_value_fenmu
        new_left_an_value = new_left_an_value.expand().simplify()
        self.steps.append(["", "当%s > 1时," % (new_latex(n))])
        self.steps.append(["", "%s = %s < %s" % (new_latex(left_an), new_latex(left_an_value), new_latex(new_left_an_value))])
        seq = sympify("t_(n)")
        self.steps.append(["", "设%s = %s, 则" % (new_latex(seq), new_latex(new_left_an_value))])
        stepsolver2 = ShuLieQiuHe().solver([seq, new_left_an_value], 1, n)
        self.steps += stepsolver2.steps
        self.label.update(stepsolver2.label)
        n_sums = stepsolver2.output[0].sympify()
        assert len(n_sums) == 1
        n_sums = n_sums[0]
        min_answer = solve_shulie_ineq([n_sums, op, right])
        if min_answer == 1:
            self.steps.append(["", "∴不等式成立"])
        self.label.add("证明数列不等式-指数型放缩法")
        return self


class ShuLieProveIneq002(BaseFunction):
    """
    设各项均为正数的数列\\{a_{n}\\}的前n项和为S_{n},满足4S_{n}=a_{n+1}^2-4n-1,a_{2},a_{5},a_{14}成等比数列,a_{1}=1.证明:\\frac{1}{a_{1}*a_{2}}+\\frac{1}{a_{2}*a_{3}}+…+ \\frac{1}{a_{n}*a_{n+1}}<\\frac{1}{2}.
    """
    def solver(self, *args):
        assert len(args) == 1
        assert isinstance(args[0], BaseSeqIneq)
        left, op, right = args[0].value
        right = sympify(right)
        assert "\u2026" in left
        left_items = inf_sums_items(left)
        left_an = left_items[-1]
        stepsolver1 = ShuLieGetSeqPoly(self.known).solver(BasePoly(left_an))
        self.steps += stepsolver1.steps
        self.label.update(stepsolver1.label)
        left_an_values = stepsolver1.output[0].sympify()
        assert len(left_an_values) == 1
        left_an_value = left_an_values[0]
        left_a1_value = left_an_value.subs({n: 1})
        if Rel(left_a1_value, right, op):
            self.steps.append(["", "当%s = 1时,不等式成立" % (new_latex(n))])
        seq = sympify('t_(n)')
        self.steps.append(["", "令%s = %s,则" % (new_latex(seq), new_latex(left_an_value))])
        stepsolver2 = ShuLieQiuHe().solver([seq, left_an_value], 1, n)
        self.steps += stepsolver2.steps
        self.label.update(stepsolver2.label)
        n_sums = stepsolver2.output[0].sympify()
        assert len(n_sums) == 1
        n_sums = n_sums[0]
        min_answer = solve_shulie_ineq([n_sums, op, right])
        if min_answer == 1:
            self.steps.append(["", "∴不等式成立"])
        self.label.add("证明数列不等式")
        return self


class ShuLieProveIneq003(BaseFunction):
    """
    设数列\\{a_{n}\\}的前n项和为S_{n},已知{a_1}=1 ,2S_{n}=na_{n+1}-\\dfrac{1}{3}{n^3}-n^2-\\dfrac{2n}{3}.证明:\\dfrac{1}{a_1}+\\dfrac{1}{a_2}+ … +\\dfrac{1}{a_n}<\\dfrac{7}{4}.
    """
    def solver(self, *args):
        assert len(args) == 1
        assert isinstance(args[0], BaseSeqIneq)
        left, op, right = args[0].value
        right = sympify(right)
        assert "\u2026" in left
        left_items = inf_sums_items(left)
        left_an = left_items[-1]
        stepsolver1 = ShuLieGetSeqPoly(self.known).solver(BasePoly(left_an))
        self.steps += stepsolver1.steps
        self.label.update(stepsolver1.label)
        left_an_values = stepsolver1.output[0].sympify()
        assert len(left_an_values) == 1
        left_an_value = left_an_values[0]
        left_a1_value = left_an_value.subs({n: 1})
        if Rel(left_a1_value, right, op):
            self.steps.append(["", "当%s = 1时,不等式成立" % (new_latex(n))])
        left_an_value_flag, left_an_fenzhi, left_an_fenmu = judge_fraction_fangsuo001(left_an_value)
        assert left_an_value_flag
        new_left_an_value = (4*left_an_fenzhi) / (4*left_an_fenmu-1)
        new_left_an_value = new_left_an_value.expand().simplify()
        self.steps.append(["", "当%s > 1时," % (new_latex(n))])
        self.steps.append(["", "%s = %s < %s" % (new_latex(left_an), new_latex(left_an_value), new_latex(new_left_an_value))])
        seq = sympify("t_(n)")
        self.steps.append(["", "设%s = %s, 则" % (new_latex(seq), new_latex(new_left_an_value))])
        stepsolver2 = ShuLieQiuHe().solver([seq, new_left_an_value], 1, n)
        self.steps += stepsolver2.steps
        self.label.update(stepsolver2.label)
        n_sums = stepsolver2.output[0].sympify()
        assert len(n_sums) == 1
        n_sums = n_sums[0]
        min_answer = solve_shulie_ineq([n_sums, op, right])
        if min_answer == 1:
            self.steps.append(["", "∴不等式成立"])
        self.label.add("证明数列不等式-分式型放缩法")
        return self


class ShuLieProveIneq004(BaseFunction):
    """
    设数列{a_{n}}满足a_{1}=0,a_{n+1}=\\frac{1}{2-a_{n}}.设{b}_{n}=\\frac{1-\\sqrt{{a}_{n+1}}}{\\sqrt{n}},数列\\{b_{n}\\}的前n项和为S_{n},证明:S_{n}<1.
    """
    def solver(self, *args):
        assert len(args) == 1
        assert isinstance(args[0], BaseSeqIneq)
        known = dict(self.known)
        left, op, right = args[0].sympify()
        expr = left - right
        expr_xiangs = sl_xiangs(expr)
        for expr_xiang in expr_xiangs:
            new_item = sympify(expr_xiang)
            stepsolver = ShuLieGetSeqPoly(known).solver(BaseSeqPoly(new_item))
            self.steps += stepsolver.steps
            self.label.update(stepsolver.label)
            new_item_values = stepsolver.output[0].sympify()
            assert len(new_item_values) == 1
            new_item_value = new_item_values[0]
            expr = expr.subs({new_item: new_item_value})
        expr = expr.expand().simplify()
        self.steps.append(["", "即证: %s" % BaseIneqs([expr, op, S.Zero]).printing()])
        self.steps.append(["", "显然成立, 得证"])
        self.label.add("证明数列不等式")
        return self


class ShuLieProveIneq(BaseFunction):
    CLS = [ShuLieProveIneq001, ShuLieProveIneq002, ShuLieProveIneq003, ShuLieProveIneq004]
    
    def solver(self, *args):
        known = self.known
        r = None
        for cl in ShuLieProveIneq.CLS:
            try:
                r = cl(known, verbose=True).solver(*args)
                break
            except Exception:
                pass
        if not r:
            raise 'try fail'
        return r


if __name__ == '__main__':
    pass
